Section: New Results

Relative Strengths of set theory and type theory

Participants : Bruno Barras [Contact] , Benjamin Werner.

Bruno Barras also formalized common translations in proof theory: negated translations and Friedman's A-translation. This was used to build a model of (classical) ZF set theory in Coq extended with one axiom called TTDA (Type-Theoretical Description Axiom). This was done in two steps: first build a model of $IZ{F}_C$ (ZF with the collection axiom but not the excluded-middle) in Coq extended with TTDA, and then encode ZF in $IZ{F}_C$, as shown by Friedman.

The converse result: an interpretation of Coq +TTDA in ZF (with one inaccessible cardinal!) seems not possible, as TTDA in a classical setting gives a (weaker) form of the axiom of choice. Bruno Barras as devised a new axiom (called the Type-Theoretical Collection Axiom) that still allow the ZF interpretation above, but he hopes that its consistency can be proved in ZF extended with one inaccessible cardinal.

Benjamin Werner has worked with Gyesik Lee on set-theoretical models of Coq 's type theory. This work is described in a paper published in the LMCS journal [18] .